YES 1.809 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule List
  ((isSuffixOf :: Eq a => [[a]]  ->  [[a]]  ->  Bool) :: Eq a => [[a]]  ->  [[a]]  ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] _ True
isPrefixOf [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys

  isSuffixOf :: Eq a => [a ->  [a ->  Bool
isSuffixOf x y reverse x `isPrefixOf` reverse y


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule List
  ((isSuffixOf :: Eq a => [[a]]  ->  [[a]]  ->  Bool) :: Eq a => [[a]]  ->  [[a]]  ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] vw True
isPrefixOf vx [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys

  isSuffixOf :: Eq a => [a ->  [a ->  Bool
isSuffixOf x y reverse x `isPrefixOf` reverse y


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule List
  (isSuffixOf :: Eq a => [[a]]  ->  [[a]]  ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] vw True
isPrefixOf vx [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys

  isSuffixOf :: Eq a => [a ->  [a ->  Bool
isSuffixOf x y reverse x `isPrefixOf` reverse y


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xy5100), Succ(xy3700000)) → new_primPlusNat(xy5100, xy3700000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xy34000), Succ(xy370000)) → new_primMulNat(xy34000, Succ(xy370000))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xy3400), Succ(xy37000)) → new_primEqNat(xy3400, xy37000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs2(Left(xy340), Left(xy3700), app(ty_[], gb), gc) → new_esEs(xy340, xy3700, gb)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(ty_Maybe, fa), eh) → new_esEs0(xy340, xy3700, fa)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(app(ty_@2, bcd), bce), bcb) → new_esEs1(xy341, xy3701, bcd, bce)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(app(ty_Either, fd), ff), eh) → new_esEs2(xy340, xy3700, fd, ff)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(app(app(ty_@3, ed), ee), ef)) → new_esEs3(xy341, xy3701, ed, ee, ef)
new_esEs2(Right(xy340), Right(xy3700), hd, app(ty_[], he)) → new_esEs(xy340, xy3700, he)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(app(ty_Either, bdg), bdh), bag, bcb) → new_esEs2(xy340, xy3700, bdg, bdh)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs3(xy342, xy3702, bbf, bbg, bbh)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(ty_[], bah)) → new_esEs(xy342, xy3702, bah)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(ty_Maybe, bcc), bcb) → new_esEs0(xy341, xy3701, bcc)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(app(ty_@2, bde), bdf), bag, bcb) → new_esEs1(xy340, xy3700, bde, bdf)
new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(app(app(ty_@3, bh), ca), cb)) → new_esEs3(xy340, xy3700, bh, ca, cb)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(ty_[], bdc), bag, bcb) → new_esEs(xy340, xy3700, bdc)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(ty_Maybe, bba)) → new_esEs0(xy342, xy3702, bba)
new_esEs2(Right(xy340), Right(xy3700), hd, app(app(ty_@2, hg), hh)) → new_esEs1(xy340, xy3700, hg, hh)
new_esEs0(Just(xy340), Just(xy3700), app(ty_Maybe, cd)) → new_esEs0(xy340, xy3700, cd)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(app(ty_Either, bcf), bcg), bcb) → new_esEs2(xy341, xy3701, bcf, bcg)
new_esEs0(Just(xy340), Just(xy3700), app(ty_[], cc)) → new_esEs(xy340, xy3700, cc)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(ty_[], bca), bcb) → new_esEs(xy341, xy3701, bca)
new_esEs2(Left(xy340), Left(xy3700), app(app(ty_Either, gg), gh), gc) → new_esEs2(xy340, xy3700, gg, gh)
new_esEs2(Left(xy340), Left(xy3700), app(app(app(ty_@3, ha), hb), hc), gc) → new_esEs3(xy340, xy3700, ha, hb, hc)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(ty_[], df)) → new_esEs(xy341, xy3701, df)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(ty_[], eg), eh) → new_esEs(xy340, xy3700, eg)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(app(ty_Either, bbd), bbe)) → new_esEs2(xy342, xy3702, bbd, bbe)
new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(ty_Maybe, bc)) → new_esEs0(xy340, xy3700, bc)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(app(ty_@2, dh), ea)) → new_esEs1(xy341, xy3701, dh, ea)
new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(app(ty_@2, bd), be)) → new_esEs1(xy340, xy3700, bd, be)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(app(app(ty_@3, bch), bda), bdb), bcb) → new_esEs3(xy341, xy3701, bch, bda, bdb)
new_esEs0(Just(xy340), Just(xy3700), app(app(app(ty_@3, db), dc), dd)) → new_esEs3(xy340, xy3700, db, dc, dd)
new_esEs(:(xy340, xy341), :(xy3700, xy3701), ba) → new_esEs(xy341, xy3701, ba)
new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(app(ty_Either, bf), bg)) → new_esEs2(xy340, xy3700, bf, bg)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(app(ty_@2, bbb), bbc)) → new_esEs1(xy342, xy3702, bbb, bbc)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(app(app(ty_@3, fg), fh), ga), eh) → new_esEs3(xy340, xy3700, fg, fh, ga)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(app(ty_@2, fb), fc), eh) → new_esEs1(xy340, xy3700, fb, fc)
new_esEs2(Right(xy340), Right(xy3700), hd, app(app(ty_Either, baa), bab)) → new_esEs2(xy340, xy3700, baa, bab)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(app(ty_Either, eb), ec)) → new_esEs2(xy341, xy3701, eb, ec)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(ty_Maybe, bdd), bag, bcb) → new_esEs0(xy340, xy3700, bdd)
new_esEs2(Left(xy340), Left(xy3700), app(ty_Maybe, gd), gc) → new_esEs0(xy340, xy3700, gd)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(ty_Maybe, dg)) → new_esEs0(xy341, xy3701, dg)
new_esEs2(Right(xy340), Right(xy3700), hd, app(ty_Maybe, hf)) → new_esEs0(xy340, xy3700, hf)
new_esEs2(Right(xy340), Right(xy3700), hd, app(app(app(ty_@3, bac), bad), bae)) → new_esEs3(xy340, xy3700, bac, bad, bae)
new_esEs0(Just(xy340), Just(xy3700), app(app(ty_@2, ce), cf)) → new_esEs1(xy340, xy3700, ce, cf)
new_esEs2(Left(xy340), Left(xy3700), app(app(ty_@2, ge), gf), gc) → new_esEs1(xy340, xy3700, ge, gf)
new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(ty_[], bb)) → new_esEs(xy340, xy3700, bb)
new_esEs0(Just(xy340), Just(xy3700), app(app(ty_Either, cg), da)) → new_esEs2(xy340, xy3700, cg, da)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(app(app(ty_@3, bea), beb), bec), bag, bcb) → new_esEs3(xy340, xy3700, bea, beb, bec)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_isPrefixOf(:(xy330, xy331), :(xy3710, xy3711), ba) → new_isPrefixOf(xy331, xy3711, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_isPrefixOf0(xy34, xy33, xy37, :(xy3610, xy3611), ba) → new_isPrefixOf0(xy34, xy33, new_flip(xy37, xy3610, ba), xy3611, ba)

The TRS R consists of the following rules:

new_flip(xy33, xy34, ba) → :(xy34, xy33)

The set Q consists of the following terms:

new_flip(x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_isPrefixOf1(xy33, xy34, :(xy350, xy351), xy36, ba) → new_isPrefixOf1(new_flip(xy33, xy34, ba), xy350, xy351, xy36, ba)

The TRS R consists of the following rules:

new_flip(xy33, xy34, ba) → :(xy34, xy33)

The set Q consists of the following terms:

new_flip(x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: